T:Type, L:(T List), R:({x:T| (x  L)} es_realizer{i:l}).
l_all(L; T; x.R-Feasible{i:l}(R(x)))
 l_all(L; T; x.l_all(L; T; y.(R-compat{i:l}(R(x); R(y))  (x = y  T))))
 R-Feasible{i:l}
 R-Feasible(Rall(L; x.R(x))) 

latex

Definitions	A c B, x:A. B(x), x. t(x), (x  l), P  Q, False, A, A  B, lelt(i; j; k), True, T, P  Q, P  Q, int_seg(i; j), pairwise(x,y.P(x;y); L), prop{i:l}, t  T, Rall(L; x.R(x)), P  Q, x(s), l_all(L; T; x.P(x)), P  Q, x:A. B(x),
Lemmas	l all map, R-compat-self, select member, le wf, map select, length wf1, select wf, map length, true wf, squash wf, int seg wf, R-Feasible wf, R-compat wf, l member wf, es realizer wf, map wf, list-set-type, R-feasible-Rlist